Automatic many-sorted theorem proving is the process of getting a computer to agree that a particular theorem in many-sorted first-order logic is true. Conventional theorem provers that are based on resolution try to derive the empty clause from a set of clauses.
However, there are situations in which it is desirable to express properties of structures of different types (or sorts). For instance, this is the case if one is interested in axiomatizing data structures found in computer science (integers, reals, characters, stacks, queues, lists, etc). By adding to the formalism of first-order logic the notion of type (also called sort), one obtains a flexible and convenient logic called many-sorted first-order logic, which enjoys the same properties as first-order logic.
Currently, conventional theorem provers deal with many-sorted logic by standard translation to first-order logic. However, a problem with this approach is that, after the translation, the algorithm works within one domain. Working within one domain can result in an increase in the search space and slow down the search portion of the algorithm.
An example of background art in this technology area is the paper entitled: “A More Expressive Formulation of Many Sorted Logic,” by Anthony G. Cohn that suggests many-sorted logics can increase deductive efficiency by eliminating useless branches of the search space, but usually this results in reduced expressiveness. The many-sorted logic described in Cohn has several unusual features which not only increase expressiveness but also can reduce the search space even more than a conventional many-sorted logic.